This paper shows that the semantics of programs with aggregates implemented by the solvers clingo and dlv can be characterized as extended First-Order formulas with intensional functions in the logic of Here-and-There. Furthermore, this characterization can be used to study the strong equivalence of programs with aggregates under either semantics. We also present a transformation that reduces the task of checking strong equivalence to reasoning in classical First-Order logic, which serves as a foundation for automating this procedure.

In classical logic, nonBoolean fluents, such as the location of an object, can be naturally described by functions. However, this is not the case in answer set programs, where the values of functions are pre-defined, and nonmonotonicity of the semantics is related to minimizing the extents of predicates but has nothing to do with functions. We extend the first-order stable model semantics by Ferraris, Lee, and Lifschitz to allow intensional functions -- functions that are specified by a logic program just like predicates are specified. We show that many known properties of the stable model semantics are naturally extended to this formalism and compare it with other related approaches to incorporating intensional functions. Furthermore, we use this extension as a basis for defining Answer Set Programming Modulo Theories (ASPMT), analogous to the way that Satisfiability Modulo Theories (SMT) is defined, allowing for SMT-like effective first-order reasoning in the context of ASP. Using SMT solving techniques involving functions, ASPMT can be applied to domains containing real numbers and alleviates the grounding problem. We show that other approaches to integrating ASP and CSP/SMT can be related to special cases of ASPMT in which functions are limited to non-intensional ones.

In classical logic, nonBoolean fluents, such as the location of an object and the color of a ball, can be naturally described by functions, but this is not the case with the traditional stable model semantics, where the values of functions are pre-defined, and nonmonotonicity of the semantics is related to minimizing the extents of predicates but has nothing to do with functions. We extend the first-order stable model semantics by Ferraris, Lee and Lifschitz to allow intensional functions. The new formalism is closely related to multi-valued nonmonotonic causal logic, logic programs with intensional functions, and other extensions of logic programs with functions, while keeping similar properties as those of the first-order stable model semantics. We show how to eliminate intensional functions in favor of intensional predicates and vice versa, and use these results to encode fragments of the language in the input language of ASP solvers and CSP solvers.

We study a logical system FQHT that is appropriate for reasoning about nonmonotonic theories with intensional functions as treated in the approach of Bartholomew and Lee (2012). We provide a logical semantics, a Gentzen style proof theory and establish completeness results. The adequacy of the approach is demonstrated by showing that it captures the Bartholemew/Lee semantics and satisfies a strong equivalence property.

The stable model semantics treats a logic program as a mechanism for specifying its intensional predicates. In this paper we discuss a modification of that semantics in which functions, rather than predicates, are intensional. The idea of the new definition comes from nonmonotonic causal logic.

In classical logic, nonBoolean fluents, such as the location of an object and the color of a ball, can be naturally described by functions, but this is not the case with the traditional stable model semantics, where the values of functions are pre-defined, and nonmonotonicity of the semantics is related to minimizing the extents of predicates but has nothing to do with functions. We extend the first-order stable model semantics by Ferraris, Lee and Lifschitz to allow intensional functions. The new formalism is closely related to multi-valued nonmonotonic causal logic, logic programs with intensional functions, and other extensions of logic programs with functions, while keeping similar properties as those of the first-order stable model semantics. We show how to eliminate intensional functions in favor of intensional predicates and vice versa, and use these results to encode fragments of the language in the input language of ASP solvers and CSP solvers.